es:ES, e, e':E. e = e'  ([e, e'] ~ [e']) 

latex

Definitions	x:A. B(x), P  Q, [e, e'], t  T, Prop, xL. P(x), x(s), A, T, True, SQType(T), {T}, False, as @ bs, filter(P;l), Y, reduce(f;k;as), if b t else f fi, true, false, e  e' , P  Q, P  Q, P  Q, P & Q, (e <loc e'), , Unit,
Lemmas	filter append, es-ble wf, es-before wf, es-E wf, event system wf, filter is nil, not functionality wrt iff, assert wf, es-le wf, assert-es-ble, l member wf, member-es-before, es-le-not-locl, es-le-loc, es-loc wf, squash wf, true wf, es-loc-pred, es-locl-iff, not wf, es-first wf, es-locl wf, filter wf, bool wf, eqtt to assert, iff transitivity, bnot wf, eqff to assert, assert of bnot